Nuprl Lemma : interleaved_family_occurence_wf
4,23
postcript
pdf
T
,
I
:Type,
L
:(
I
(
T
List)),
L2
:
T
List,
f
:(
i
:
I
||
L
(
i
)||
||
L2
||).
interleaved_family_occurence(
T
;
I
;
L
;
L2
;
f
)
Prop
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
i
j
,
P
Q
,
False
,
A
,
A
B
,
,
Prop
,
x
:
A
.
B
(
x
)
,
l
[
i
]
,
S
T
,
S
T
,
increasing(
f
;
k
)
,
P
&
Q
,
interleaved_family_occurence(
T
;
I
;
L
;
L2
;
f
)
Lemmas
increasing
wf
,
select
wf
,
not
wf
,
non
neg
length
,
int
seg
wf
,
length
wf1
origin
T, I:Type, L:(I
(T List)), L2:T List, f:(i:I
||L(i)||||L2||).
Prop T, I:Type, L:(I(T List)), L2:T List, f:(i:I||L(i)||||L2||).
Prop Tx:A. B(x)
}
j
Q
A
B
x:A. B(x)
T
T